(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a__dbl(0) → 0
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0, cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0) → 01
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0, cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0) → 01
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0) → 0
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01) → 01
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
Rewrite Strategy: FULL
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
S is empty.
Rewrite Strategy: FULL
(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(4) Obligation:
TRS:
Rules:
a__dbl(0') → 0'
a__dbl(s(X)) → s(s(dbl(X)))
a__dbls(nil) → nil
a__dbls(cons(X, Y)) → cons(dbl(X), dbls(Y))
a__sel(0', cons(X, Y)) → mark(X)
a__sel(s(X), cons(Y, Z)) → a__sel(mark(X), mark(Z))
a__indx(nil, X) → nil
a__indx(cons(X, Y), Z) → cons(sel(X, Z), indx(Y, Z))
a__from(X) → cons(X, from(s(X)))
a__dbl1(0') → 01'
a__dbl1(s(X)) → s1(s1(a__dbl1(mark(X))))
a__sel1(0', cons(X, Y)) → mark(X)
a__sel1(s(X), cons(Y, Z)) → a__sel1(mark(X), mark(Z))
a__quote(0') → 01'
a__quote(s(X)) → s1(a__quote(mark(X)))
a__quote(dbl(X)) → a__dbl1(mark(X))
a__quote(sel(X, Y)) → a__sel1(mark(X), mark(Y))
mark(dbl(X)) → a__dbl(mark(X))
mark(dbls(X)) → a__dbls(mark(X))
mark(sel(X1, X2)) → a__sel(mark(X1), mark(X2))
mark(indx(X1, X2)) → a__indx(mark(X1), X2)
mark(from(X)) → a__from(X)
mark(dbl1(X)) → a__dbl1(mark(X))
mark(sel1(X1, X2)) → a__sel1(mark(X1), mark(X2))
mark(quote(X)) → a__quote(mark(X))
mark(0') → 0'
mark(s(X)) → s(X)
mark(nil) → nil
mark(cons(X1, X2)) → cons(X1, X2)
mark(01') → 01'
mark(s1(X)) → s1(mark(X))
a__dbl(X) → dbl(X)
a__dbls(X) → dbls(X)
a__sel(X1, X2) → sel(X1, X2)
a__indx(X1, X2) → indx(X1, X2)
a__from(X) → from(X)
a__dbl1(X) → dbl1(X)
a__sel1(X1, X2) → sel1(X1, X2)
a__quote(X) → quote(X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
(5) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
a__sel,
mark,
a__dbl1,
a__sel1,
a__quoteThey will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(6) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(7) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(8) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(9) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel.
(10) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__dbl1, a__sel1, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(11) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__dbl1(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n79116_0))) →
*3_0, rt ∈ Ω(n79116
0)
Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n79116_0, 1)))) →RΩ(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0)))))) →RΩ(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n79116_0))))) →IH
s1(s1(*3_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(12) Complex Obligation (BEST)
(13) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel1, a__sel, mark, a__quote
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(14) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel1.
(15) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__quote, a__sel, mark
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__quote(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n1977765_0))) →
*3_0, rt ∈ Ω(n1977765
0)
Induction Base:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n1977765_0, 1)))) →RΩ(1)
s1(a__quote(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))))) →RΩ(1)
s1(a__quote(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n1977765_0)))) →IH
s1(*3_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(17) Complex Obligation (BEST)
(18) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
mark, a__sel, a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol mark.
(20) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel, a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel.
(22) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__dbl1, a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(23) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
a__dbl1(
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(
+(
1,
n3958080_0))) →
*3_0, rt ∈ Ω(n3958080
0)
Induction Base:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, 0)))
Induction Step:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, +(n3958080_0, 1)))) →RΩ(1)
s1(s1(a__dbl1(mark(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0)))))) →RΩ(1)
s1(s1(a__dbl1(s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(n3958080_0))))) →IH
s1(s1(*3_0))
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(24) Complex Obligation (BEST)
(25) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
The following defined symbols remain to be analysed:
a__sel1
They will be analysed ascendingly in the following order:
a__sel = mark
a__sel = a__dbl1
a__sel = a__sel1
a__sel = a__quote
mark = a__dbl1
mark = a__sel1
mark = a__quote
a__dbl1 = a__sel1
a__dbl1 = a__quote
a__sel1 = a__quote
(26) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)
Could not prove a rewrite lemma for the defined symbol a__sel1.
(27) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(28) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
(29) BOUNDS(n^1, INF)
(30) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(31) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n3958080_0))) → *3_0, rt ∈ Ω(n39580800)
(32) BOUNDS(n^1, INF)
(33) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
a__quote(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n1977765_0))) → *3_0, rt ∈ Ω(n19777650)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(34) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
(35) BOUNDS(n^1, INF)
(36) Obligation:
TRS:
Rules:
a__dbl(
0') →
0'a__dbl(
s(
X)) →
s(
s(
dbl(
X)))
a__dbls(
nil) →
nila__dbls(
cons(
X,
Y)) →
cons(
dbl(
X),
dbls(
Y))
a__sel(
0',
cons(
X,
Y)) →
mark(
X)
a__sel(
s(
X),
cons(
Y,
Z)) →
a__sel(
mark(
X),
mark(
Z))
a__indx(
nil,
X) →
nila__indx(
cons(
X,
Y),
Z) →
cons(
sel(
X,
Z),
indx(
Y,
Z))
a__from(
X) →
cons(
X,
from(
s(
X)))
a__dbl1(
0') →
01'a__dbl1(
s(
X)) →
s1(
s1(
a__dbl1(
mark(
X))))
a__sel1(
0',
cons(
X,
Y)) →
mark(
X)
a__sel1(
s(
X),
cons(
Y,
Z)) →
a__sel1(
mark(
X),
mark(
Z))
a__quote(
0') →
01'a__quote(
s(
X)) →
s1(
a__quote(
mark(
X)))
a__quote(
dbl(
X)) →
a__dbl1(
mark(
X))
a__quote(
sel(
X,
Y)) →
a__sel1(
mark(
X),
mark(
Y))
mark(
dbl(
X)) →
a__dbl(
mark(
X))
mark(
dbls(
X)) →
a__dbls(
mark(
X))
mark(
sel(
X1,
X2)) →
a__sel(
mark(
X1),
mark(
X2))
mark(
indx(
X1,
X2)) →
a__indx(
mark(
X1),
X2)
mark(
from(
X)) →
a__from(
X)
mark(
dbl1(
X)) →
a__dbl1(
mark(
X))
mark(
sel1(
X1,
X2)) →
a__sel1(
mark(
X1),
mark(
X2))
mark(
quote(
X)) →
a__quote(
mark(
X))
mark(
0') →
0'mark(
s(
X)) →
s(
X)
mark(
nil) →
nilmark(
cons(
X1,
X2)) →
cons(
X1,
X2)
mark(
01') →
01'mark(
s1(
X)) →
s1(
mark(
X))
a__dbl(
X) →
dbl(
X)
a__dbls(
X) →
dbls(
X)
a__sel(
X1,
X2) →
sel(
X1,
X2)
a__indx(
X1,
X2) →
indx(
X1,
X2)
a__from(
X) →
from(
X)
a__dbl1(
X) →
dbl1(
X)
a__sel1(
X1,
X2) →
sel1(
X1,
X2)
a__quote(
X) →
quote(
X)
Types:
a__dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
0' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
nil :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
cons :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbls :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
mark :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
indx :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
from :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
01' :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
s1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
a__quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
dbl1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
sel1 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
quote :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
hole_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote1_0 :: 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0 :: Nat → 0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote
Lemmas:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
Generator Equations:
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(0) ⇔ 0'
gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(x, 1)) ⇔ s(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(x))
No more defined symbols left to analyse.
(37) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
a__dbl1(gen_0':s:dbl:nil:cons:dbls:sel:indx:from:01':s1:dbl1:sel1:quote2_0(+(1, n79116_0))) → *3_0, rt ∈ Ω(n791160)
(38) BOUNDS(n^1, INF)